FIG. 1 illustrates a prior art binary simulation verification environment. Referring to FIG. 1, a series of stimulus, referred to herein as stimulus1–stimulusM, are applied to a device under test (DUT) 101. The stimuli are usually values that are to be assigned to specific input ports of DUT 101 at specific times. In response to the series of stimulus, a series of corresponding outputs are generated, referred to herein as output1–outputM. Each of the output1–outputM represents sets of values that are output on the output ports of DUI 101, where such sets in each output of output1–outputM corresponds to a particular time and in response to a particular set of stimulus values, in particular, one of stimulus1–stimulusM. The series of stimulus, stimulus1–stimulusM, are also applied to a reference model 102, which generates a series of expected outputs, referred to herein as expected—output1–expected—outputM, respectively. The outputs, output1–outputM, generated by DUT 101 are compared to expected—output1–expected—outputM to verify that DUT 101 is operating as expected.
Hardware Description Language (HDL) simulators/accelerators are the primary tools used to simulate and verify the designs described in HDL, such as Verilog HDL or VHDL. Most of popular software tools such as NCVerilog of Cadence Corporation of San Jose, Calif., VCS of Synopsys of Mountain View, Calif., and Modelsim of Mentor Graphics of Wilsonville, Oreg. are designed to speed up the simulation of a single testcase. Some are for the hardware accelerators and emulators such as emulators from Cadence and Quickturn. Similarly, U.S. Pat. Nos. 5,752,000 or 6,138,266 describe accelerators and emulators. Methods and tools both in research and commercial forms have been devised to do parallel simulation of a HDL design, which requires more than one physical processor to achieve any speedup in performing the simulation.
Some simulation tools claim to be able to simulate multiple stimuli by using 1 or 2 bits per stimulus for a computer with multiple bits such as 32-bit machines. Such a method could allow one to simultaneously simulate more than 1 stimuli but not more than 32 stimuli at the same time.
Traditional symbolic simulation is another technique used for formal verification. In the traditional symbolic simulation, the input stimulus is always thought to be encoded as variables.
Symbolic model checking, similar to symbolic simulation, assumes the inputs to take free variables with proper constraints (if there is any) at each clock cycle.